/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.formula;

import chameleon.gameSolver.NuGat.NuGatInterface;
import java.io.IOException;

/**
 * This class represents an operator for a formula. To add a new operator, just
 * add a Tag in @formula.Tag.java and edit the method convert2Tag.
 *
 * This class do also a link between NuGat and Chameleon. The method encOp return
 * the tag corresponding, in NuGat, to the operator.
 *
 *
 * @author simon
 */
public class Operator {

    private String graphOp_;
    private int operator_;
    private boolean unary_;
    private NuGatInterface nugat_;

    public Operator(String op) {
        graphOp_ = op;
        operator_ = convert2Tag(graphOp_);
    }

    public void setNugat(NuGatInterface nugat){
        nugat_ = nugat;
    }

    public boolean isUnary(){
        return unary_;
    }

    private int convert2Tag(String op) {
        if (op.equals(Tag.S_AND)){
            unary_ = false;
            return Tag.AND;
        }
        else if (op.equals(Tag.S_OR)){
            unary_ = false;
            return Tag.OR;
        }
        else if (op.equals(Tag.S_NEXT)){
            unary_ = true;
            return Tag.NEXT;
        }

        else if (op.equals(Tag.S_NEXT_TRANSITION)){
            unary_ = true;
            return Tag.NEXT_TRANSITION;
        }

        else if (op.equals(Tag.S_ASSIGN)){
            unary_ = false;
            return Tag.ASSIGN;
        }
        else if (op.equals(Tag.S_UNTIL)){
            unary_ = false;
            return Tag.UNTIL;
        }
        else if (op.equals(Tag.S_EVENTUALLY)){
            unary_ = true;
            return Tag.EVENTUALLY;
        }
        else if (op.equals(Tag.S_ALWAYS)){
            unary_ = true;
            return Tag.ALWAYS;
        }
        else if (op.equals(Tag.S_NOT)){
            unary_ = true;
            graphOp_ = "~";
            return Tag.NOT;
        }
        else if (op.equals(Tag.S_IMPLIES)){
            unary_ = false;
            return Tag.IMPLIES;
        }
        else if (op.equals(Tag.S_EQUIVALENCE)){
            unary_ = false;
            return Tag.EQUIVALENCE;
        }
        else if(op.equals(Tag.S_PLUS)){
            unary_=false;
            return Tag.PLUS;
        }
        else if(op.equals(Tag.S_MINUS)){
            unary_=false;
            return Tag.MINUS;
        }
        else if(op.equals(Tag.S_MUL)){
            unary_=false;
            return Tag.MUL;
        }
        else if(op.equals(Tag.S_DIVIDE)){
            unary_=false;
            return Tag.DIVIDE;
        }
        else if(op.equals(Tag.S_MINUS_UNARY)){
            unary_=true;
            return Tag.MINUS_UNARY;
        }
        else if(op.equals(Tag.S_NOTEQUAL)){
            unary_=false;
            return Tag.NOTEQUAL;
        }
        else if(op.equals(Tag.S_EQUAL)){
            unary_=false;
            return Tag.EQUAL;
        }
        else if (op.equals(Tag.S_LT)){
            unary_ = false;
            return Tag.LT;
        }        
        else if (op.equals(Tag.S_GT)){
            unary_ = false;
            return Tag.GT;
        }
        else if (op.equals(Tag.S_LE)){
            unary_ = false;
            return Tag.LE;
        }
        else if (op.equals(Tag.S_GE)){
            unary_ = false;
            return Tag.GE;
        }
        else
            throw new RuntimeException("OPERATOR::unknow operator : "+op);
    }

    @Override
    public String toString(){
        if (graphOp_.equals(Tag.MINUS_UNARY))
            return "-";
        else
            return graphOp_;
    }

    public int getTag(){
        return operator_;
    }

    public boolean isEquals (int operator){
        return operator == operator_;
    }

    public boolean isTemporal(){
        return (Tag.ALWAYS == operator_ || Tag.EVENTUALLY == operator_
                ||Tag.NEXT == operator_ || Tag.UNTIL == operator_ );
    }

    /**
     * this function return the corresponding Tag in Nugat for an operator
     * in the transition relation.
     *
     * @return
     * @throws IOException
     */

    public int encOp() {
        switch(operator_){
            case (chameleon.model.formula.Tag.AND):
                return nugat_.AND;
            case (chameleon.model.formula.Tag.OR):
                return nugat_.OR;
            case (chameleon.model.formula.Tag.IMPLIES):
                return nugat_.IMPLIES;
            case (chameleon.model.formula.Tag.EQUIVALENCE):
                return nugat_.IFF;
            case (chameleon.model.formula.Tag.ASSIGN):
                return nugat_.EQUAL;
            case (chameleon.model.formula.Tag.NOTEQUAL):
                return nugat_.NOTEQUAL;
            case (chameleon.model.formula.Tag.NEXT):
                return nugat_.OP_NEXT;
            case (chameleon.model.formula.Tag.NEXT_TRANSITION):
                return nugat_.NEXT;
            case (chameleon.model.formula.Tag.NOT):
                return nugat_.NOT;
            case (chameleon.model.formula.Tag.PLUS):
                return nugat_.PLUS;
            case (chameleon.model.formula.Tag.MINUS):
                return nugat_.MINUS;
            case (chameleon.model.formula.Tag.DIVIDE):
                return nugat_.DIVIDE;
            case (chameleon.model.formula.Tag.MUL):
                return nugat_.TIMES;
            case (chameleon.model.formula.Tag.ALWAYS):
                return nugat_.OP_GLOBAL;
            case (chameleon.model.formula.Tag.EVENTUALLY):
                return nugat_.OP_FUTURE;
            case (chameleon.model.formula.Tag.LT):
                return nugat_.LT;
            case (chameleon.model.formula.Tag.GT):
                return nugat_.GT;
            case (chameleon.model.formula.Tag.LE):
                return nugat_.LE;
            case (chameleon.model.formula.Tag.GE):
                return nugat_.GE;
            case (chameleon.model.formula.Tag.EQUAL):
                return nugat_.EQUAL;
            default:
                return -1;
        }
    }
}
